$\forall$${\it es}$:ES, ${\it e'}$:E, $P$:(\{$e$:E$\mid$ loc($e$) = loc(${\it e'}$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\\[0ex]$\exists$$e$$<$${\it e'}$.$P$($e$) $\Leftarrow\!\Rightarrow$ (($\neg$($\uparrow$first(${\it e'}$))) c$\wedge$ ($P$(pred(${\it e'}$)) $\vee$ $\exists$$e$$<$pred(${\it e'}$).$P$($e$)))